\begin{tabbing}
$\vdash$  \=$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)), $x$:$A$, $n$:$\mathbb{N}$.\+
\\[0ex]($\uparrow$can{-}apply($f$;$x$)) $\Rightarrow$ (($f$\^{}$n$+1($x$)) $\sim$ ($f$\^{}$n$(do{-}apply($f$;$x$))))
\-
\end{tabbing}